REF, NoConds \\[0ex]Unfolds ``\$abs`` \$hyp $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Unfolds ``\$abs`` ( \$hyp)$\cdot$